T:Type, L1, L2:(T List). interleaving(T;L1;L2;L1 @ L2) 

latex

Definitions	t  T, P & Q, interleaving(T;L1;L2;L), x:A. B(x), disjoint_sublists(T;L1;L2;L), suptype(S; T), S  T, , x:A. B(x), P  Q, P  Q, P  Q, increasing(f;k), True, T, {i..j}
Lemmas	append wf, non neg length, length append, not wf, select wf, increasing wf, length wf1, int seg wf, id increasing, select append front, le wf, squash wf, select append back